Dependent type checking fallback #5
Conversation
maxkurze1
force-pushed
the
typechecking
branch
from
1fc23bb
to
ea0820b
Compare
coq/Frontend.v
Outdated
| vm_compute (arg); | ||
| vm_compute (ret); | ||
| vm_compute (body) |
There was a problem hiding this comment.
Even using vm_compute here turns out to be too aggressive in certain situations;
Working on a patch... probably fixed in a couple of minutes
maxkurze1
force-pushed
the
typechecking
branch
from
ea0820b
to
5673488
Compare
|
Now the tactic uses |
|
There is still some work to do here. It would be nice to abstract the proof term and only keep the fact that it exists. |
|
Please provide a hint database to register manual proofs. |
Type checking for dependent Koika functions
The default type checker only tries to construct the checked term by using
vm_compute. However, when a Koika function depends on some variable, says, this check will get stuck on a term likeforall s, ... EqDec.ec_dec s s .... This equality is rather computed than proven, but for this computation it is necessary to know the exact value of s.To circumvent this problem (and it is really more a workaround than a solution), I built a tactic, that carefully computes the type leaving
eq_decoccurrences untouched. These occurrences are then (if possible) rewritten with a proof.This workaround is incorporated into the normal type checking algorithm as a fallback, in other words, the type checker will first try to construct the term using
vm_compute(which should be faster) and only if this fails it will try to compute it using the new tactic.